module sum_n
  (
   //input wire	      clk_in, reset_n,
   input wire [7:0]   m_in, n_in, 
   output wire [15:0] s_out
   );

   // Определение констант
   //wire [7:0] one = 1;
//   localparam one = 1;
//   localparam two = 2;
   
   //constant two = 2;

   // Входные порты a и b
   //wire 7:0 m_in;
   //wire 7:0 n_in;

   // Выходной порт S
   //
   // wire 15:0 s_out;

   // Расчет значения s
//   assign s_out = (m_in + n_in)  *  (n_in - m_in + one) / two;
   assign s_out = (n_in>=m_in)&(n_in>0)&(m_in>0)?(m_in + n_in) * (n_in - m_in + 1) / 2:0;   
`ifdef FORMAL
    // Formal properties here
   localparam [2:0]        FORMAL_TEST = 3'b000;
   case (FORMAL_TEST)
     3'b000: begin
	always @(*) begin
	   assume(s_out>=1);
	   //assert((m_in>0)&(n_in>0)&(n_in>m_in));
	   assert(m_in>0);
	   assert(n_in>0);
	   assert(n_in>=m_in);
	end
     end
     3'b001: begin
	// No extra logic

	// Never passes
     end
     3'b010: begin
     end
     3'b011: begin

     end
     3'b100: begin

     end
     3'b101: begin

     end
     3'b110: begin

     end
     3'b111: begin

     end
     endcase
`endif   
endmodule // calculator
